|
|
Proof Systems: A Study on Form and Complexity
Jalali Keshavarz, Raheleh ; Pudlák, Pavel (advisor) ; Metcalfe, George (referee) ; Ramanayake, Revantha (referee)
Proof Systems: A Study on Form and Complexity This dissertation includes three parts. The first two parts are related to each other. In [2] and [1], Iemhoff introduced a connection between the existence of a terminating sequent calculus of a certain kind and the uniform inter- polation property of the super-intuitionistic logic that the calculus captures. In the second part, we will generalize this relationship to also cover the sub- structural setting on the one hand and a more powerful type of systems called semi-analytic calculi, on the other. To be more precise, we will show that any sufficiently strong substructural logic with a semi-analytic calculus has Craig interpolation property and in case that the calculus is also terminating, it has uniform interpolation. This relationship then leads to some concrete applications. On the positive side, it provides a uniform method to prove the uniform interpolation property for the logics FLe, FLew, CFLe, CFLew, IPC, CPC and some of their K and KD-type modal extensions. However, on the negative side the relationship finds its more interesting application to show that many sub-structural logics including Ln, Gn, BL, R and RMe , al- most all super-intutionistic logics (except at most seven of them) and almost all extensions of S4 (except thirty seven of them) do not...
|
|
|
Efficient Representation of Program States
Jančík, Pavel ; Kofroň, Jan (advisor) ; Gargantini, Angelo (referee) ; Barnat, Jiří (referee)
Při verifikaci programů se snažíme rozhodnout, zda program obsahuje či neobsahuje chyby. Základním předpokladem všech verifikačních postupů je efektivní reprezentace a manipulace se stavy programů. V této práci představujeme techniky pro nalezení nepodstatných informací ve stavech programů a pro jejich odstranění. Tato práce obsahuje redukce vhodné pro explicitní i symbolickou reprezentaci stavů. Naše postupy vhodné pro explicitní reprezentaci byly speciálně navrženy pro vícevláknové programy. Naše analýzy dokáží nalézt takové hodnoty v dynamicky alokovaných objektech, tedy na haldě, které program již nebude v následujících krocích číst. Logické formule v predikátové nebo výrokové logice jsou převažující symbolickou reprezentací množin stavů programu. Craigovy interpolanty jsou jedním z obvyklých postupů pro získání formulí s požadovanými vlastnostmi. V této práci představujeme nový způsob jejich výpočtu, který používá přiřazení proměnných pro zmenšení jejich velikosti. Pomocí přiřazení proměnných můžeme zablokovat ty cesty v programu, které nechceme, aby interpolant bral v potaz a tím zmenšit jejich velikost.
|
|
|
Efficient Representation of Program States
Jančík, Pavel ; Kofroň, Jan (advisor) ; Gargantini, Angelo (referee) ; Barnat, Jiří (referee)
Při verifikaci programů se snažíme rozhodnout, zda program obsahuje či neobsahuje chyby. Základním předpokladem všech verifikačních postupů je efektivní reprezentace a manipulace se stavy programů. V této práci představujeme techniky pro nalezení nepodstatných informací ve stavech programů a pro jejich odstranění. Tato práce obsahuje redukce vhodné pro explicitní i symbolickou reprezentaci stavů. Naše postupy vhodné pro explicitní reprezentaci byly speciálně navrženy pro vícevláknové programy. Naše analýzy dokáží nalézt takové hodnoty v dynamicky alokovaných objektech, tedy na haldě, které program již nebude v následujících krocích číst. Logické formule v predikátové nebo výrokové logice jsou převažující symbolickou reprezentací množin stavů programu. Craigovy interpolanty jsou jedním z obvyklých postupů pro získání formulí s požadovanými vlastnostmi. V této práci představujeme nový způsob jejich výpočtu, který používá přiřazení proměnných pro zmenšení jejich velikosti. Pomocí přiřazení proměnných můžeme zablokovat ty cesty v programu, které nechceme, aby interpolant bral v potaz a tím zmenšit jejich velikost.
|
|
|
Methods for reduction of Craig's interpolant size using partial variable assignment
Blicha, Martin ; Kofroň, Jan (advisor) ; Kučera, Petr (referee)
Abstract. Since the introduction of interpolants to the field of symbolic model checking, interpolation-based methods have been successfully used in both hardware and software model checking. Recently, variable assignments have been introduced to the computation of interpolants. In the context of abstract reachability graphs, variable assignment can be used not only to prevent out-of-scope variables from appearing in interpolants, but also to reduce the size of the interpolant significantly. We further extend the framework for computing interpolants under variable assignment, prove the correctness of the system and show that it has potential to further decrease the size of the computed interpolants. At the end we analyze under which conditions the computed interpolants will still have the path interpolation property, a desired property in many interpolation-based techniques. 1
|
guest ::
